Adding Spanish translation - #30
Conversation
El objetivo de esta herramienta es dar a los estudiantes una forma de aprender a hacer demostraciones para luego ser capaces de escribirlas a papel, es decir, transportar sus conocimientos de Lean al examen. Luego no tiene sentido enseñarles una sintaxis diferente de la que ellos usarán el día que tengan que escribirlo, por ello se cambia la conjunción copulativa "con" a "yy" ya que "y" solamente da problemas si se llama a una variable "y".
Expanded the README to provide detailed project information, usage instructions, and links to resources.
pepamontero
left a comment
pepamontero
left a comment
There was a problem hiding this comment.
I’ve left a few suggestions focused on Spanish natural phrasing.
This is not a complete review, but rather a collection of smaller issues I noticed while reading. Most of them are minor wording improvements to make the Spanish sound more natural and consistent with standard mathematical usage.
I'm happy to take another pass if you find this helpful, or discuss any of the suggestions.
pepamontero
left a comment
pepamontero
left a comment
There was a problem hiding this comment.
Hemos estado mirando un poco más en grupo durante nuestra reunión de MadLean (@madlean-hub), te dejo dos comentarios muy pequeños jajaja.
Hemos estado hablando del tema de la "y", definitivamente poner "yy" es un poco raro, hemos pensado que en el caso de intro quizás sería más fácil poner solo comas? También podría haber una forma de diferenciar la y de variable de la y de and porque la y siempre va sin comas alrededor (a y b versus. x, y, z y w), pero habría que cambiar probablemente cosas del repo original (no sólo el lenguaje) e igual habría que preguntar primero. No se si te parece complicarse mucho la vida.
También creemos que al archivo de calc le falta un poco de revisión, pero es un poco difícil verlo en la sintaxis aparte (se ve mucho más claro cuando lees un ejemplo completo). Igual se podría intentar escribir más ejemplos para ver.
| open Lean Verbose.Spanish | ||
|
|
||
| namespace Verbose.Named | ||
| scoped macro ("Hecho" <|> "Afirmación") name:ident ":" stmt:term "por" colGt prf:tacticSeq: tactic => |
There was a problem hiding this comment.
Aquí quizás quedaría mejor "Se tiene" o "Tenemos".
There was a problem hiding this comment.
Creo que entraría en conflicto con la sintaxis "Por h se tiene x", tengo que ver si es posible. De todas formas, aunque estoy de acuerdo que Hecho/Afirmación puede sonar raro ya que corta el ritmo de la lectura, creo que tiene sentido al escribirlo por que estas enunciando una afirmación que va a parte de la demostración. No sé tampoco si Se tiene funcionaria mejor.
Intentaré escribir más ejemplos y os comento.
There was a problem hiding this comment.
Dándole otra pensada a esto, en realidad sí que estoy de acuerdo en que en muchos libros ponen en medio de una demostración algo tipo
Afirmación: lalala
pero igual en este caso tendría sentido que fuera de la forma:
Ejemplo: ...
Demostración:
intro ...
otras tacticas
Afirmación: ...
Demostración:
....
QED
seguimos con la demo inicial
como para que quedase más claro. No se si esa es el uso normal ya.
There was a problem hiding this comment.
Por el momento, las demostraciones de los facts solo se indentan en todos los idiomas. Yo lo dejaría así y si eso se añade lo del QED en otra PR. Por otra parte, qué te parece llamarlos simplemente Afirmaciones y quitar lo de Hecho?
| scoped macro ("Hecho" <|> "Afirmación") name:ident ":" stmt:term "pues" prf:maybeAppliedES : tactic => do | ||
| withRef name `(tactic|(checkName $name; have $name : $stmt := by Concluimos por $prf)) | ||
|
|
||
| scoped macro ("Hecho" <|> "Afirmación") name:ident ":" stmt:term "por cálculo" : tactic => do |
There was a problem hiding this comment.
Aquí hemos pensado que quizás se podría poner "desarrollando" en lugar de "por cálculo".
There was a problem hiding this comment.
(Se me olvidó comentar esto). Me gusta la idea por que queda más natural pero creo que "por cálculo" mantiene la cohesión interna con "Calc". Aunque igual queda forzado creo que es más intuitivo.
Este tema es complicado pero la idea que proponéis no es mala. De todas formas, en el repositorio original alguien ya preguntó por algo parecido y Patrick dijo que no cree que fuese posible. Igual no se barajó esta solución así que voy a proponérsela a ver si él sabe por dónde empezar y cómo hacerlo de forma que no cambie los otros idiomas.
Siendo honestos, con ese archivo hice un apaño por que tiene muchos conectores de implicación (por, ya que, pues) que puse un poco como pude (y que a decir verdad tampoco entiendo cuándo toca poner uno u otro). La cosa es que la traducción del inglés al francés me dio la misma impresión (ya le preguntaré a Patrick). Al final no le di mucha importancia ya que en la mayoría de casos se usa "por", pero habría que revisarlo para que sea coherente. Estaría bien poder usar la misma palabra (por) y que Lean entienda cual es la "táctica" por el contexto pero no lo tengo claro. Lo pruebo y os confirmo. Intentaré ver eso primero y hacer algunos ejemplos más para pasarooslos. |
|
Genial, gracias por responder tan rápido! Es muy buen trabajo y yo creo que con algo de tiempo puede salir algo muy chulo. Cualquier cosa nos dices, si te viene bien que miremos algo en concreto hacemos algún hueco; como no estamos super metidos en el proyecto tampoco sabemos bien cuáles son las cosas más importantes. Pero nos encantará ayudar :) |
Now it is a separator allowing `,y` or `,e`.
|
Hola @pepamontero , he cambiado como funciona la conjunción AND, ahora mismo acepta |
|
Hola @navimath ! Perdona que he estado de vacaciones y con cierto lío! Además durante el verano no tenemos sesiones de MadLean así que no puedo contrastar. Pero lo intento mirar un poco y te digo! |
pepamontero
left a comment
pepamontero
left a comment
There was a problem hiding this comment.
Hola! Estoy haciendo una revisión más detallada de la traducción! Aquí te pongo algunos comentarios. Todavía me faltan algunos archivos: Help (lo he dejado a la mitad), Widget, ExampleLib y Examples.
Pero como es bastante voy publicando esta mitad. Sobre lo de el "y" tengo alguna idea, luego escribo otro comentario más detallado al respecto.
En general está muy bien!! Muchas gracias por tu trabajo :))
Thanks to @pepamontero for her feedback :) Co-authored-by: Pepa Montero Jimena <pepamonterojimena@gmail.com>
|
He visto tus respuestas y te he respondido:) En cuanto pueda sigo mirando el resto. Sobre lo de la y: la solución actual no me parece mal. Pero la verdad es que no me convence del todo! O sea como que es un poco raro al final tener que poner ",y" cada vez que quieras poner y. Pero es una posible solución. Te comento otra idea, a ver qué opinas. Pero siéntete libre de decirme que no te gusta jajajaja. Se me ocurre que quizás se podría utilizar otra letra que sea parecida a la y, como po ejemplo: ỿ o у. (Esta última no es exactamente y, es de otro alfabeto, puedes comprobarlo con la búsqueda jajaja). Obviamente escribir estas letras es un rollo, pero por lo que tengo entendido, la extensión de VS Code tiene unas opciones que permiten añadir entradas adicionales a las traducciones de tipo \N -> ℕ. Se podría añadir una entrada {"y": "ỿ"} de manera que al escribir \y se escribiese automáticamente ỿ. Y creo que esto se podría poner como configuración dentro solo de la carpeta en Español, para que los que usan la versión española les afecte y a los demás no. Pero no soy experta así que todo esto podría ser imposible en realidad jajaja. Algunos problemas que podría tener esto:
Quizás todos estos problemas se solucionarían-ish si dejásemos ambas opciones? No lo se. Para la e se podría hacer lo mismo, aunque también está la opción de retirar completamente el e, que tampoco lo veo mal porque realmente como tampoco hay normas de aplicación en realidad tampoco aporta mucho más y tampoco creo que haya muchos casos en los que haga falta. |
Igual usar
Ahora mismo es así
El problema que le veo es que hay que editar el .json de la extensión de VS (aunque es fácil y verbose lean funciona bien), y no se puede restringir solamente al proyecto de verbose, menos a una carpeta. Una solución sería pedir al usuario que editase su extensión para añadirlo (tipo "añade esta linea a tus settings") y luego estaría que falte soporte para la |
Arreglos:
- `Como … se tiene` → `obtenemos` (introduce objetos, con `tal que`)
- `Como … se tiene` → `se tiene que` (deriva hechos)
- `Decidimos en función de si` → `Distinguimos en casos según si`
- `Probemos que W basta` → `Probemos que se cumple para W`
Nuevo vocabulario:
- `Por … se tiene` desaparece; quedan `tenemos` y `obtenemos`
- `Hecho` desaparece; `Afirmación` es la única keyword de afirmación
- `Calc` → `Por desarrollo`, `Calc?` → `Por desarrollo?`
- `por cálculo` → `por cuentas` como justificación de un paso;
`por desarrollo` se rechaza dentro del bloque (sería circular),
pero `Afirmación` acepta las dos formas
- `Calculemos`/`Calculamos` → `Desarrollemos`/`Desarrollamos`
- `Desarrollamos` (unfold) → `Desplegamos`/`Despleguemos
2 participants
-- Edited on 17 August.
This PR translates the widget, help and error messages and adapts custom tactics to the Spanish language, see the list of (most of) translated commands:
Calc has not been translated since it can be interpreted as in "Cálculo".
However, to avoid problems with the infamous translation of "and" (since in Spanish is just "y" which would clash with the variable name), I took the decision of naming it as
,yas well adding a,eto avoid havingx ,y y.I would like your feedback on this translation before merging.